↳ ITRS
↳ ITRStoIDPProof
z
eval_1(x, y, z) → Cond_eval_1(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
Cond_eval_11(TRUE, x, y, z) → eval_1(x, y, -@z(x, y))
Cond_eval_1(TRUE, x, y, z) → eval_1(+@z(x, y), y, z)
Cond_eval_0(TRUE, x, y, z) → eval_1(x, y, z)
eval_0(x, y, z) → Cond_eval_0(>@z(y, 0@z), x, y, z)
eval_1(x, y, z) → Cond_eval_11(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
z
eval_1(x, y, z) → Cond_eval_1(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
Cond_eval_11(TRUE, x, y, z) → eval_1(x, y, -@z(x, y))
Cond_eval_1(TRUE, x, y, z) → eval_1(+@z(x, y), y, z)
Cond_eval_0(TRUE, x, y, z) → eval_1(x, y, z)
eval_0(x, y, z) → Cond_eval_0(>@z(y, 0@z), x, y, z)
eval_1(x, y, z) → Cond_eval_11(&&(&&(>@z(y, x), >@z(z, y)), >@z(y, 0@z)), x, y, z)
(0) -> (2), if ((y[0] →* y[2])∧(z[0] →* z[2])∧(+@z(x[0], y[0]) →* x[2]))
(0) -> (3), if ((y[0] →* y[3])∧(z[0] →* z[3])∧(+@z(x[0], y[0]) →* x[3]))
(1) -> (2), if ((y[1] →* y[2])∧(-@z(x[1], y[1]) →* z[2])∧(x[1] →* x[2]))
(1) -> (3), if ((y[1] →* y[3])∧(-@z(x[1], y[1]) →* z[3])∧(x[1] →* x[3]))
(2) -> (1), if ((z[2] →* z[1])∧(x[2] →* x[1])∧(y[2] →* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →* TRUE))
(3) -> (0), if ((z[3] →* z[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →* TRUE))
(4) -> (5), if ((z[4] →* z[5])∧(x[4] →* x[5])∧(y[4] →* y[5])∧(>@z(y[4], 0@z) →* TRUE))
(5) -> (2), if ((y[5] →* y[2])∧(z[5] →* z[2])∧(x[5] →* x[2]))
(5) -> (3), if ((y[5] →* y[3])∧(z[5] →* z[3])∧(x[5] →* x[3]))
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDependencyGraphProof
z
(0) -> (2), if ((y[0] →* y[2])∧(z[0] →* z[2])∧(+@z(x[0], y[0]) →* x[2]))
(0) -> (3), if ((y[0] →* y[3])∧(z[0] →* z[3])∧(+@z(x[0], y[0]) →* x[3]))
(1) -> (2), if ((y[1] →* y[2])∧(-@z(x[1], y[1]) →* z[2])∧(x[1] →* x[2]))
(1) -> (3), if ((y[1] →* y[3])∧(-@z(x[1], y[1]) →* z[3])∧(x[1] →* x[3]))
(2) -> (1), if ((z[2] →* z[1])∧(x[2] →* x[1])∧(y[2] →* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →* TRUE))
(3) -> (0), if ((z[3] →* z[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →* TRUE))
(4) -> (5), if ((z[4] →* z[5])∧(x[4] →* x[5])∧(y[4] →* y[5])∧(>@z(y[4], 0@z) →* TRUE))
(5) -> (2), if ((y[5] →* y[2])∧(z[5] →* z[2])∧(x[5] →* x[2]))
(5) -> (3), if ((y[5] →* y[3])∧(z[5] →* z[3])∧(x[5] →* x[3]))
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
z
(2) -> (1), if ((z[2] →* z[1])∧(x[2] →* x[1])∧(y[2] →* y[1])∧(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)) →* TRUE))
(3) -> (0), if ((z[3] →* z[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →* TRUE))
(0) -> (3), if ((y[0] →* y[3])∧(z[0] →* z[3])∧(+@z(x[0], y[0]) →* x[3]))
(0) -> (2), if ((y[0] →* y[2])∧(z[0] →* z[2])∧(+@z(x[0], y[0]) →* x[2]))
(1) -> (3), if ((y[1] →* y[3])∧(-@z(x[1], y[1]) →* z[3])∧(x[1] →* x[3]))
(1) -> (2), if ((y[1] →* y[2])∧(-@z(x[1], y[1]) →* z[2])∧(x[1] →* x[2]))
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
(1) (y[2]=y[1]∧-@z(x[1], y[1])=z[3]∧y[1]=y[3]∧x[2]=x[1]∧z[2]=z[1]∧x[1]=x[3]∧&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z))=TRUE ⇒ COND_EVAL_11(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL_11(TRUE, x[1], y[1], z[1])≥EVAL_1(x[1], y[1], -@z(x[1], y[1]))∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))
(2) (>@z(y[2], 0@z)=TRUE∧>@z(y[2], x[2])=TRUE∧>@z(z[2], y[2])=TRUE ⇒ COND_EVAL_11(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL_11(TRUE, x[2], y[2], z[2])≥EVAL_1(x[2], y[2], -@z(x[2], y[2]))∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))
(3) (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)
(4) (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)
(5) (y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)
(6) (y[2] + -1 + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -1 + (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)
(7) (y[2] + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)
(8) (y[2] + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0)
(9) (y[2] + x[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] + x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + (2)y[2] + z[2] + x[2] ≥ 0)
(10) (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ (-1)Bound + y[2] + z[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧1 + x[2] + (2)y[2] + z[2] ≥ 0)
(11) (y[2]=y[1]∧x[2]=x[1]∧-@z(x[1], y[1])=z[2]1∧z[2]=z[1]∧x[1]=x[2]1∧y[1]=y[2]1∧&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z))=TRUE ⇒ COND_EVAL_11(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL_11(TRUE, x[1], y[1], z[1])≥EVAL_1(x[1], y[1], -@z(x[1], y[1]))∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))
(12) (>@z(y[2], 0@z)=TRUE∧>@z(y[2], x[2])=TRUE∧>@z(z[2], y[2])=TRUE ⇒ COND_EVAL_11(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL_11(TRUE, x[2], y[2], z[2])≥EVAL_1(x[2], y[2], -@z(x[2], y[2]))∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥))
(13) (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)
(14) (y[2] + -1 ≥ 0∧y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0∧-2 + z[2] + y[2] + (-1)x[2] ≥ 0)
(15) (y[2] + -1 + (-1)x[2] ≥ 0∧-1 + z[2] + (-1)y[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -2 + z[2] + y[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-2 + (-1)Bound + z[2] + (-1)x[2] ≥ 0)
(16) (y[2] + -1 + (-1)x[2] ≥ 0∧z[2] ≥ 0∧y[2] + -1 ≥ 0 ⇒ -1 + (2)y[2] + z[2] + (-1)x[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧-1 + (-1)Bound + y[2] + z[2] + (-1)x[2] ≥ 0)
(17) (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)
(18) (y[2] ≥ 0∧z[2] ≥ 0∧x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)
(19) (y[2] ≥ 0∧z[2] ≥ 0∧(-1)x[2] + y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + (-1)x[2] + (2)y[2] + z[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + y[2] + z[2] ≥ 0)
(20) (x[2] + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0∧x[2] ≥ 0 ⇒ 1 + x[2] + (2)y[2] + z[2] ≥ 0∧(UIncreasing(EVAL_1(x[1], y[1], -@z(x[1], y[1]))), ≥)∧(-1)Bound + x[2] + y[2] + z[2] ≥ 0)
(21) (EVAL_1(x[2], y[2], z[2])≥NonInfC∧EVAL_1(x[2], y[2], z[2])≥COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])∧(UIncreasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥))
(22) ((UIncreasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)
(23) ((UIncreasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)
(24) ((UIncreasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧1 ≥ 0)
(25) (0 = 0∧0 = 0∧0 = 0∧(UIncreasing(COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])), ≥)∧0 = 0∧1 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0)
(26) (EVAL_1(x[3], y[3], z[3])≥NonInfC∧EVAL_1(x[3], y[3], z[3])≥COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))
(27) ((UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)
(28) ((UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)
(29) (0 ≥ 0∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0)
(30) (0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))
(31) (z[0]=z[3]1∧+@z(x[0], y[0])=x[3]1∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧y[0]=y[3]1∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(32) (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(33) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)
(34) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)
(35) (-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)
(36) (-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)
(37) (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)
(38) (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)
(39) (y[3] ≥ 0∧z[3] ≥ 0∧(-1)x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)x[3] + y[3] ≥ 0∧0 ≥ 0)
(40) (x[3] + y[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
(41) (z[0]=z[2]∧y[0]=y[2]∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧+@z(x[0], y[0])=x[2]∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(42) (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(43) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)
(44) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧0 ≥ 0∧y[3] ≥ 0)
(45) (-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)
(46) (-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧y[3] ≥ 0∧0 ≥ 0)
(47) (y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
(48) (y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
(49) (y[3] + x[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + y[3] ≥ 0∧0 ≥ 0)
(50) (y[3] ≥ 0∧z[3] ≥ 0∧x[3] + y[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + x[3] + y[3] ≥ 0∧0 ≥ 0)
POL(-@z(x1, x2)) = x1 + (-1)x2
POL(0@z) = 0
POL(EVAL_1(x1, x2, x3)) = -1 + x3 + (-1)x1
POL(COND_EVAL_1(x1, x2, x3, x4)) = -1 + x4 + (-1)x2
POL(TRUE) = -1
POL(&&(x1, x2)) = -1
POL(+@z(x1, x2)) = x1 + x2
POL(FALSE) = -1
POL(undefined) = -1
POL(>@z(x1, x2)) = -1
POL(COND_EVAL_11(x1, x2, x3, x4)) = -1 + x4 + (-1)x2 + x1
COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1]))
COND_EVAL_11(TRUE, x[1], y[1], z[1]) → EVAL_1(x[1], y[1], -@z(x[1], y[1]))
EVAL_1(x[2], y[2], z[2]) → COND_EVAL_11(&&(&&(>@z(y[2], x[2]), >@z(z[2], y[2])), >@z(y[2], 0@z)), x[2], y[2], z[2])
EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])
&&(FALSE, FALSE)1 ↔ FALSE1
-@z1 ↔
+@z1 ↔
&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
z
(3) -> (0), if ((z[3] →* z[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →* TRUE))
(0) -> (3), if ((y[0] →* y[3])∧(z[0] →* z[3])∧(+@z(x[0], y[0]) →* x[3]))
(0) -> (2), if ((y[0] →* y[2])∧(z[0] →* z[2])∧(+@z(x[0], y[0]) →* x[2]))
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
z
(3) -> (0), if ((z[3] →* z[0])∧(x[3] →* x[0])∧(y[3] →* y[0])∧(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)) →* TRUE))
(0) -> (3), if ((y[0] →* y[3])∧(z[0] →* z[3])∧(+@z(x[0], y[0]) →* x[3]))
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)
(1) (EVAL_1(x[3], y[3], z[3])≥NonInfC∧EVAL_1(x[3], y[3], z[3])≥COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))
(2) ((UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)
(3) ((UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)
(4) (0 ≥ 0∧0 ≥ 0∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))
(5) (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(UIncreasing(COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0)
(6) (z[0]=z[3]1∧+@z(x[0], y[0])=x[3]1∧x[3]=x[0]∧y[3]=y[0]∧&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z))=TRUE∧y[0]=y[3]1∧z[3]=z[0] ⇒ COND_EVAL_1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL_1(TRUE, x[0], y[0], z[0])≥EVAL_1(+@z(x[0], y[0]), y[0], z[0])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(7) (>@z(y[3], 0@z)=TRUE∧>@z(y[3], x[3])=TRUE∧>@z(z[3], y[3])=TRUE ⇒ COND_EVAL_1(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL_1(TRUE, x[3], y[3], z[3])≥EVAL_1(+@z(x[3], y[3]), y[3], z[3])∧(UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥))
(8) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)
(9) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)
(10) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧-1 + z[3] + (-1)y[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧1 + (-1)Bound + (2)z[3] + (-1)y[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)
(11) (-1 + y[3] ≥ 0∧-1 + y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧3 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧-1 + y[3] ≥ 0)
(12) (y[3] ≥ 0∧y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧y[3] ≥ 0)
(13) (y[3] ≥ 0∧y[3] + (-1)x[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + (-1)x[3] ≥ 0∧y[3] ≥ 0)
(14) (y[3] ≥ 0∧y[3] + x[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] + x[3] ≥ 0∧y[3] ≥ 0)
(15) (x[3] + y[3] ≥ 0∧y[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0 ⇒ (UIncreasing(EVAL_1(+@z(x[0], y[0]), y[0], z[0])), ≥)∧4 + (-1)Bound + y[3] + (2)z[3] ≥ 0∧x[3] + y[3] ≥ 0)
POL(0@z) = 0
POL(EVAL_1(x1, x2, x3)) = 1 + (2)x3 + (-1)x2 + (-1)x1
POL(COND_EVAL_1(x1, x2, x3, x4)) = 1 + (2)x4 + (-1)x3 + (-1)x2
POL(TRUE) = 0
POL(&&(x1, x2)) = 1
POL(+@z(x1, x2)) = x1 + x2
POL(FALSE) = 0
POL(undefined) = -1
POL(>@z(x1, x2)) = -1
COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])
COND_EVAL_1(TRUE, x[0], y[0], z[0]) → EVAL_1(+@z(x[0], y[0]), y[0], z[0])
EVAL_1(x[3], y[3], z[3]) → COND_EVAL_1(&&(&&(>@z(y[3], x[3]), >@z(z[3], y[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
&&(FALSE, FALSE)1 → FALSE1
+@z1 ↔
&&(TRUE, TRUE)1 → TRUE1
&&(TRUE, FALSE)1 → FALSE1
&&(FALSE, TRUE)1 → FALSE1
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
z
eval_1(x0, x1, x2)
Cond_eval_11(TRUE, x0, x1, x2)
Cond_eval_1(TRUE, x0, x1, x2)
Cond_eval_0(TRUE, x0, x1, x2)
eval_0(x0, x1, x2)